$\forall$$V$:(Id$\rightarrow$Type), $M_{1}$, $M_{2}$:MsgA.
\\[0ex]($\forall$$x$:Id. $V$($x$) $\subseteq$r $M_{2}$.ds($x$)) $\Rightarrow$ $M_{1}$ $\subseteq$ $M_{2}$ $\Rightarrow$ ($\forall$$x$:Id, $v$:($\mathbb{Q}\rightarrow$$V$($x$)). $M_{2}$.init($x$,$v$) $\Rightarrow$ $M_{1}$.init($x$,$v$))